a, b:. ((a * b) = 0)  ((a = 0)  (b = 0)) 

latex

Up	int 2, int 2
Definitions	, t  T, P  Q, x:A. B(x), P  Q, a  b  T , , Dec(P), False, A
Lemmas	decidable int equal, nequal wf, mul cancel in eq